Nuprl Lemma : zero_ann_b
12,41
postcript
pdf
a
,
b
:
. (
((
a
*
b
) = 0))
((
(
a
= 0)) & (
(
b
= 0)))
latex
ProofTree
Definitions
,
t
T
,
P
&
Q
,
A
,
P
Q
,
x
:
A
.
B
(
x
)
,
False
Lemmas
not
wf
origin
a, b:
. (
((a * b) = 0)) 
(((a = 0)) & ((b = 0)))
a, b:. (((a * b) = 0)) (((a = 0)) & ((b = 0)))
TA Qx:A. B(x)